Termination w.r.t. Q proof of /tmp/tmpOcr8Z9/Ex2_8

Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(f, x)
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(f, x)
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(subst, f), g), x) → APP(f, x) we obtained the following new rules:

APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(subst, f), g), x) → APP(g, x) we obtained the following new rules:

APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(fix, f), x) → APP(f, app(fix, f)) we obtained the following new rules:

APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ MNOCProof

                        ↳ QDP

                          ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

s = APP(app(app(subst, x0), app(fix, y_0)), x2) evaluates to t =APP(app(y_0, app(fix, y_0)), x2)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Matcher: [ ]
Semiunifier: [y_0 / app(subst, x0)]

Rewriting sequence

APP(app(app(subst, x0), app(fix, app(subst, x0))), x2) → APP(app(fix, app(subst, x0)), x2)
with rule APP(app(app(subst, x0'), app(fix, y_0)), x2') → APP(app(fix, y_0), x2') at position [] and matcher [x0' / x0, x2' / x2, y_0 / app(subst, x0)]

APP(app(fix, app(subst, x0)), x2) → APP(app(app(subst, x0), app(fix, app(subst, x0))), x2)
with rule APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.